ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da).
ecl-halt(ds;da;x)  (event-info(ds;da) List)Prop 

latex

Definitions	x:A. B(x), t  T, , event-info(ds;da), Prop, ecl-halt(ds;da;x), P & Q, x:A. B(x), A, let x,y,z = a in t(x;y;z), A & B, P  Q, P  Q, AB, x,y. t(x;y), x. t(x), SQType(T), {T}, x,y,z,w. t(x;y;z;w), False, x,y,z. t(x;y;z), Valtype(da;k), x(s1,s2), x(s1,s2,s3,s4), x(s1,s2,s3), x(s)
Lemmas	ecl ind wf, nat wf, event-info wf, decl-state wf, ma-valtype wf, append wf, fpf-cap wf, Kind-deq wf, top wf, assert wf, l all wf, not wf, Knd sq, subtype rel self, bool wf, le wf, iseg wf, star-append wf, l member wf, l exists wf, ecl wf, fpf wf, Knd wf, Id wf